\documentclass[12pt]{article}
\usepackage[utf8x]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[frenchb]{babel}
\usepackage{graphicx}
\usepackage[section]{placeins}
\usepackage{fancyhdr}
\usepackage{hyperref}
\usepackage{amssymb}
\hypersetup{
     backref=true,    %permet d'ajouter des liens dans...
     pagebackref=true,%...les bibliographies
     hyperindex=true, %ajoute des liens dans les index.
     colorlinks=true, %colorise les liens
     breaklinks=true, %permet le retour à la ligne dans les liens trop longs
     urlcolor= blue,  %couleur des hyperliens
     linkcolor= blue %couleur des liens internes
}

%%%% debut macro pour enlever le nom chapitre %%%%
\makeatletter
\def\@makechapterhead#1{%
  \vspace*{20\p@}%
  {\parindent \z@ \raggedright \normalfont
    \interlinepenalty\@M
    \ifnum \c@secnumdepth >\m@ne
        \Huge\bfseries \thechapter\quad
    \fi
    \Huge \bfseries #1\par\nobreak
    \vskip 40\p@
  }}

\def\@makeschapterhead#1{%
  \vspace*{50\p@}%
  {\parindent \z@ \raggedright
    \normalfont
    \interlinepenalty\@M
    \Huge \bfseries  #1\par\nobreak
    \vskip 40\p@
  }}
\makeatother
%%%% fin macro %%%%

\newlength{\plarg}
\setlength{\plarg}{14cm}
\newlength{\glarg}
\setlength{\glarg}{17cm}

\pagestyle{fancy}
\fancyhf{}
\fancyhead[C]{}
 %En-tête de page
 \renewcommand{\headrulewidth}{0.5pt}
\addtolength{\headheight}{15pt} % 
\lhead{\leftmark}
\chead{}
\rhead{\includegraphics[width = 20mm, scale=1]{img/univ-nantes}}

%Pieds de page
\lfoot{\textit{Formal Software}}
\cfoot{\textit{\thepage}}
\rfoot{\textsc{Bizet - Chaline}}


\renewcommand{\contentsname}{Sommaire}
\renewcommand{\listfigurename}{Illustrations}


\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%		Page de garde		%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{titlepage}
\thispagestyle{empty}
\begin{center}
\begin{minipage}{\plarg}
\vspace{1cm} \centering
Master Alma 2 \\
2012 - 2013 \vspace{1cm}
\end{minipage}
\end{center}

\begin{center}
  \begin{minipage}{\plarg}
    \vspace{2cm} \centering
    \rule{\linewidth{}}{0.3mm}\\
    \vspace{1mm}
    {\huge Formal Software  }\\
    \vspace{5mm}
    {\large Protocole de transfert de messages entre un Client et un Serveur}
    \rule{\linewidth{}}{0.3mm}\\
    \bsc{Chaline} Jérémy\\
    \bsc{Bizet} Jonathan
    \begin{center}
    	\includegraphics[scale=0.3]{img/qrcode}
    \end{center}
  \end{minipage}
 \end{center}

  \begin{center}
    \begin{minipage}{\plarg}
      \vspace{2cm} \centering
    \end{minipage}
  \end{center}

  \vfill \hspace{-1cm}
\begin{minipage}[c]{0.55\linewidth}
 {\rule{\plarg}{0.5pt}}\\
    \footnotesize{Professeurs Encadrants:}\\
    \small{Mr Claude \bsc{Jard}}\\		
\end{minipage} \hfill
\begin{minipage}[c]{0.40\linewidth}
   \hfill \includegraphics[width = 20mm, scale=1]{img/univ-nantes}
\end{minipage}\leftmark
\end{titlepage}
\thispagestyle{empty}
\tableofcontents
\clearpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%	Fin page de garde	%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\setcounter{page}{1}
\section{Introduction}
Le but du projet était de formaliser un systeme composé de intenté client server modélisés par deux automates (voir figure \ref{fig:schCS}). 
Ses deux automates comminiquent entre eux par par echange de message dans des canneaux \emph {FIFO}.

\begin{figure}[htb]
  \centering
   \includegraphics[scale=.4]{img/automate}
  \caption{Schéma de la communication Client-Serveur}
  \label{fig:schCS}.
\end{figure}

\newpage
\section{Les canaux bornés}

La figure \ref{fig:graph} est la représentation du graphe de simulation exhaustive du protocole. 

La figure \ref{fig:petri} représente le graphe de marquage après modélisation du protocole avec un réseau de pétri, avec échange de message par le biais d'un tas.
\begin{figure}[htb]
  \centering
  \includegraphics[scale=0.7]{img/graphe}
  \caption{Graphe de simulation exhaustive}
  \label{fig:graph}
\end{figure}

\begin{figure}[htb]
  \centering
  \includegraphics[scale=0.4]{img/graphDeMarquage}
  \caption{Graphe de marque avec un tas}
  \label{fig:petri}
\end{figure}

Nous constatons que les deux graphes sont isomorphe donc nous pouvons conclure que les canaux sont bornés.

\clearpage
\newpage
\section{Modélisation dans roméo}
\begin{center}

\end{center}
\begin{figure}[htb]
  \centering
  \includegraphics[scale=0.7]{img/reseauPetri}
  \caption{Modélisation du protocole avec Romeo}
  \label{fig:resPetr}
\end{figure}

\newpage
\section{Spécification en logique temporelle}
Soient les deux propositions devant être exprimés en logique temporelle : 
\begin{enumerate}
	\item \textbf{Le protocole peut toujours revenir à l’état initial}.
	\newline
	\newline
	En donnant au mot \emph{pouvoir} son sens premier, c'est à dire \emph{capacité, possibilité}, alors la première proposition est toujours vrai. Mais si nous envisagons des blocages liés à des évènement extérieurs, tel qu'un envoie infini de messages, alors, il est possible que le protocole ne puisse pas revenir à l'état initial, mais cette affirmation repose sur l'unique hyposthèse d'une mauvaise interprétation du mot \emph{pouvoir}.
	\newline
	\newline
	Soit i l'état où l'automate (A ou B) est dans l'état final. La première proposition s'exprime de la façon suivante : $  \square \Diamond i$
	\newline
	\item \textbf{Entre deux états où les processus A et B sont en attente, il existe un état où A est déconnecté}.
	\newline
	\newline
	 Soit \emph{a} l'état où \emph{A} et \emph{B} sont en attente, et \emph{$d_A$} tout état du système où \emph{A} est déconnecté, la partie gauche de la formule suivante correspond à "soit un état du système où A et B sont en attente, suivit dans le futur d'un autre même état", alors, celà implique la partie gauche, la négation de : "il n'y a pas l'évènement où A est deconnecté suivit d'une attente de A et de B".
	\newline
	\newline
	$  \square ((a \wedge \bigcirc \Diamond a) => (\neg(\neg d_A \cup a )))$
\end{enumerate}

\newpage
\section{Implémentation de AxB : Client-Serveur}
\subsection{Choix techniques}
	Afin de simuler le fonctionnement de deux automates, nous avons choisis d'utiliser deux threads communiquant par un PIPE\footnote{Un PIPE, ou un tube, est un mécanisme de communication inter-processus sous la forme d'une série de données, octets ou bits, accessibles en FIFO.}, qui permet une gestion FIFO des messages.
	L'automate client sitch\footnote{Instruction qui permet d'effectuer un branchement à partir de la valeur d'une variable.} sur son état courant, en agissant selon la situation :
\begin{itemize}
	\item \emph{Dans l'état 0}, l'automate attend une action de l'utilisateur pour demander une connexion.
	\item \emph{Dans l'état 1}, l'automate attend que le serveur lui réponde, s'il accepte ou non la connexion.
	\item \emph{Dans l'état 2}, l'automate attend une action de l'utilisateur:
	\begin{enumerate}
		\item soit un \emph{envoie de message}, qui passera le client dans l'état 3 et le mettra en attente d'une réponse du serveur.
		\item soit une \emph{demande de deconnexion}, qui passera le client dans l'état 0 et lui permettra de demander une nouvelle connexion, sans attendre de réponse du serveur.
	\end{enumerate}
	\item \emph{Dans l'état 3}, il attend que le serveur lui confirme la réception du message par un acquittement.
\end{itemize}

Lors de la lecture de messages dans la file, que ce soit le client ou le serveur, un contrôle est effectué, déclenchant une erreur si un imprévu se produit. Même si dans le cadre de l'utilisation classique par l'IHM ce n'est pas possible, nous avons envisager la lecture d'un fichier contenu une suite d'instructions. La classe ReadFile lit un fichier, parse\footnote{Analyse syntaxique du contenu du fichier et séparation des instructions sur un caractère donné, ici le caractère \emph{;}} les instructions, et fournit un itérateur sur ces instructions, permettant au programme de les executer à tour de rôle.

\subsection{IHM}
\begin{figure}[htb]
  \centering
  \includegraphics[scale=1]{screen/mainWindow}
  \caption{Fenêtre principal de l'application}
  \label{fig:scrnMW}.
\end{figure}

Cette fenêtre permet d'agire en tant que client et d'envoyer des messages au serveur :
\begin{itemize}
	\item \emph{Demande connexion} : envoie une requête de connexion au serveur. Uniquement utilisable si le client est dans l'état 0, le fait passer à l'état 1 et le met en attente d'une réponse du serveur.
	\item \emph{Envoyer data} : simule l'action d'envoie de message du client vers le serveur, utilisable uniquement si le client est dans l'état 2, le fait passer dans l'état 3 et le met en attente d'un acquitement du serveur.
	\item \emph{Fin} : envoie au serveur la notification d'une fin de connexion, utilisable uniquement dans l'état 3, le fait passer dans l'état 0, et permet de redemander une connexion sans attendre de réponse du serveur.
\end{itemize}

\begin{figure}[htb]
  \centering
  \includegraphics[scale=1]{screen/altWindow}
  \caption{Fenêtre donnant une vue des actions côté serveur}
  \label{fig:scrnAW}.
\end{figure}

Cette fenêtre permet d'afficher les informations côté serveur, tel que son état, les messages recus du client et ceux qui vont être envoyés.

\clearpage
\listoffigures
\clearpage

\end{document}